Álgebra de Tipos

Daniel Yokomizo / @dyokomizo

http://dyokomizo.github.io/talks

Álgebra


a = (b × c) + d
  • Símbolos: a, b, c, d
  • Operações: ×, +
  • Propriedades: comutatividade, associatividade
  • Estruturas: Monóides, Grupos, Anéis

Tipos


data Either a b = Left  a
                | Right b

data Pair a b   = Pair (a, b)
  • Variáveis: a, b
  • Construtores: Left, Right, Pair

Álgebra de Tipos

Faz sentido? Sim.

Como?

  • Definição de álgebra: estudo de estruturas algébricas
  • Estruturas algébricas: conjunto com uma ou mais operações e propriedades

Álgebra de Tipos

  • Conjunto: tipos possíveis
  • Operações: +, ×
  • Propriedades: ??
  • Estruturas: ??

Álgebra de Tipos — Primitivos

  • 1: tipo com um único habitante 
    data () = () -- aka Unit
  • 0: tipo com nenhum habitante 
    data Void -- requer EmptyDataDecls

Álgebra de Tipos — Operações

  • +: União 
    |
  • ×: Tupla 
    (,)
  • ^: Função 
    →

Álgebra de Tipos — Operações

+


data Either a b = Left  a
                | Right b
					

c = a + b

Álgebra de Tipos — Operações

×


data Pair a b   = Pair (a, b)
					

c = a × b

Álgebra de Tipos — Operações

^


data Fun a b   = Fun (a → b)
					

c = ba

Álgebra de Tipos — Exemplos


data Maybe a = Just a
             | Nothing -- () impĺícito
					

c = a + 1

Álgebra de Tipos — Exemplos


data Bool = True
          | False
					

a = 1 + 1

Álgebra de Tipos — Propriedades

Elemento neutro


a ≅ (a × 1) ≅ (1 × a)
					

String ≅ (String, ()) ≅ ((), String)
					

a ≅ (a + 0) ≅ (0 + a)
					

String ≅ (Either String Void) ≅ (Either Void String)

Álgebra de Tipos — Propriedades

Associatividade


a × (b × c) ≅ (a × b) × c
					

(String,(Int,Bool)) ≅ ((String,Int),Bool)
					

a + (b + c) ≅ (a + b) + c
					

Either String (Either Int Bool) ≅ Either (Either String Int) Bool

Álgebra de Tipos — Propriedades

Elemento neutro


a ≅ (a × 1) ≅ (1 × a)
					

a ≅ (a + 0) ≅ (0 + a)

Associatividade


a × (b × c) ≅ (a × b) × c
					

a + (b + c) ≅ (a + b) + c

Álgebra de Tipos — Estruturas

Monóide

  • Definição: conjunto com uma operação associativa e com elemento neutro
  • × com 1
  • + com 0

Álgebra de Tipos — Propriedades

Distributividade


a × (b + c) ≅ (a × b) + (a × c)
					

(String, Either Int Bool) ≅ Either (String, Int) (String, Bool)

Álgebra de Tipos — Exemplos


data A a b = A1 a b
           | A2 b
					

type A a b = Either (a, b) b
					

c = (a × b) + b
  ≅ (a × b) + (1 × b) -- Elemento neutro
  ≅ (a + 1) × b       -- Distributividade
					

type A a b = (Maybe a, b)

Álgebra de Tipos — Funções


a → b   ≍   ba
					

Bool → Int   ≍   IntBool

Álgebra de Tipos — Funções


Bool → a   ≍   aBool
					

Bool   ≍   1 + 1
					

aBool   ≅ a‌1 + 1
        ≅ a‌1 × a‌1
        ≅ a × a
					

Bool → a   ≅   (a,a)

Álgebra de Tipos — Funções


meaningOfLife :: Boolean -> Int
meaningOfLife True  = 42
meaningOfLife False = 37

Bool -> a ≅ (a, a)

meaningOfLife' :: (Int, Int)
meaningOfLife' = (42,37)

Referências